\begin{tabbing}
$\forall$\=${\it es}$:event\_system\{i:l\}, $l$:IdLnk, ${\it tgs}$:(Id List), ${\it da}$:fpf(Knd; $k$.Type),\+
\\[0ex]$f_{1}$,$f_{2}$:(\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = source($l$) $\in$ Id\} $\rightarrow$(\=(${\it tg}$:Id\+
\\[0ex]$\times$ fpf{-}cap(\=${\it da}$; Kind{-}deq; rcv($l$,${\it tg}$); void\+
\\[0ex])) List)),
\-\-\\[0ex]${\it ds}_{1}$,${\it ds}_{2}$:fpf(Id; $x$.Type).
\-\\[0ex]fpf{-}sub(Id; $x$.Type; id{-}deq; ${\it ds}_{2}$; ${\it ds}_{1}$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = source($l$) $\in$ Id\} . $f_{1}$($e$) = $f_{2}$($e$))
\\[0ex]$\Rightarrow$ with decls ${\it ds}_{1}$ ${\it da}$sends on $l$ from $e$ include $f_{1}$($e$) and only these for tags in ${\it tgs}$
\\[0ex]$\Rightarrow$ with decls ${\it ds}_{2}$ ${\it da}$sends on $l$ from $e$ include $f_{2}$($e$) and only these for tags in ${\it tgs}$
\end{tabbing}